package sketch.specs.symbc;

import gov.nasa.jpf.symbc.SolvedPCResults;

import java.util.List;
import java.util.Map;

import sketch.jpf.symbc.SymbolicJPF;
import sketch.specs.SymbolicFileParser;
import junit.framework.Test;
import junit.framework.TestCase;
import junit.framework.TestSuite;

public class SymbolicJPFOtherTypesTest extends TestCase {
	
	public static Test suite() {
		return new TestSuite(SymbolicJPFOtherTypesTest.class);
	}
	
	public void testBooleanType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassBoolean.class, MyClassBoolean.class, "myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);
		
		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);
		
		
		assertEquals(4, solvedIntValues.size());
		assertEquals(4, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));
		
	}
	
	public void testFloatType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassFloat.class, MyClassFloat.class, "myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);
		
		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);
		
		
		assertEquals(9, solvedIntValues.size());
		assertEquals(9, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));
		
		SolvedPCResults.reset();
	}
	
	public void testLongType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassLong.class, MyClassLong.class, "myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);
		
		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);
		
		
		assertEquals(5, solvedIntValues.size());
		assertEquals(5, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));
		
		SolvedPCResults.reset();
	}
	
	public void testDoubleType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassDouble.class, MyClassDouble.class,
				"myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);

		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);

		assertEquals(13, solvedIntValues.size());
		assertEquals(13, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));

		SolvedPCResults.reset();
	}
	
	public void testByteType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassByte.class, MyClassByte.class,
				"myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);

		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);

		assertEquals(4, solvedIntValues.size());
		assertEquals(4, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));

		SolvedPCResults.reset();
	}
	
	public void testCharType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassChar.class, MyClassChar.class,
				"myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);

		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);

		assertEquals(5, solvedIntValues.size());
		assertEquals(5, solvedRealValues.size());
		
//		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
//				SymbolicFileParser.convertToNestedList(solvedRealValues));

		assertTrue(SymbolicFileParser.convertToNestedList(solvedIntValues).size() ==
			SymbolicFileParser.convertToNestedList(solvedRealValues).size());
		
		SolvedPCResults.reset();
	}
	
	public void testShortType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassShort.class, MyClassShort.class,
				"myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);

		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);

		assertEquals(2, solvedIntValues.size());
		assertEquals(2, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));

		SolvedPCResults.reset();
	}
	
	public void testCombineType() {
		SolvedPCResults.reset();
		SymbolicJPF.execute(MyClassIntFloat.class, MyClassIntFloat.class, "myMethod");
		List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
		System.out.println("Solved int results are: " + solvedIntValues);

		List<Map<String, Double>> solvedRealValues = SolvedPCResults.solvedRealValues;
		System.out.println("Solved real results are: " + solvedRealValues);

		assertEquals(6, solvedIntValues.size());
		assertEquals(6, solvedRealValues.size());
		
		SymbolicFileParser.checkTwoListValidity(SymbolicFileParser.convertToNestedList(solvedIntValues),
				SymbolicFileParser.convertToNestedList(solvedRealValues));

		SolvedPCResults.reset();
	}
}